Nuprl Lemma : es-leaks_wf
11,40
postcript
pdf
es
:ES{i},
e
,
e'
:E,
x
:Id.
e
leaks
x
to
e'
{i'}
latex
Definitions
A
c
B
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
e
leaks
x
to
e'
,
,
t
T
,
x
:
A
.
B
(
x
)
,
P
Q
Lemmas
event
system
wf
,
Id
wf
,
es-val
wf
,
es-valtype
wf
,
es-sender
wf
,
es-E
wf
,
es-isrcv
wf
,
assert
wf
,
es-rcv-atom
wf
,
es-state-when-without
wf
,
es-state-without
wf
,
free-from-atom
wf1
,
not
wf
,
es-loc
wf
,
es-atom
wf
origin
es:ES{i}, e, e':E, x:Id. e leaks x to e' 
{i'} es:ES{i}, e, e':E, x:Id. e leaks x to e' {i'} 
B
x:A. B(x) Tx:A. B(x)
Q